ns:(MaName List), A, B:Realizer. A  B  A|ns  B|ns 

latex

Definitions

Rplus-right(x1), Rplus-left(x1), P  Q, P & Q, T, P  Q, P  Q, True, {T}, SQType(T), , i  j , False, A, A  B, P  Q, t  T, x:A. B(x), A c B, ff, tt, Rnone?(x1), if b then t else f fi , Y, Rplus?(x1), A  B, , Dec(P), , S  T

Lemmas

nat plus inc, R-sub-self, R-sub-plus-right2, R-sub-plus-left2, R-plus wf, R-sub transitivity, R-restrict-Rnone, true wf, squash wf, Rnone-implies, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, bool sq, bool cases, bnot wf, bool wf, Rnone? wf, assert wf, not wf, Rplus wf, Rplus-right wf, Rplus-left wf, R-restrict wf, R-plus-sub, Rplus-implies, R-size-decreases, ge wf, nat properties, Rplus? wf, decidable assert, nat plus wf, le wf, es realizer wf, R-sub wf, R-size wf, nat wf, MaName wf